\functions {
 int a_LSBRCK_0_RSBRCK_, a_LSBRCK_1_RSBRCK_, a, b_LSBRCK_0_RSBRCK_, b_LSBRCK_1_RSBRCK_, b, c_LSBRCK_0_RSBRCK_, c_LSBRCK_1_RSBRCK_, cin, c, cout1, d, BITADDER_LSBRCK_0_RSBRCK__S1, BITADDER_LSBRCK_0_RSBRCK__C2, B_LSBRCK_0_RSBRCK_, BITADDER_LSBRCK_1_RSBRCK__C2, BITADDER_LSBRCK_1_RSBRCK__S1, A_LSBRCK_1_RSBRCK_, B_LSBRCK_1_RSBRCK_, COUT1, BITADDER_LSBRCK_1_RSBRCK__C1, BITADDER_COUT_LSBRCK_0_RSBRCK_, C_LSBRCK_1_RSBRCK_, A_LSBRCK_0_RSBRCK_, COUT, BITADDER_LSBRCK_0_RSBRCK__C1, CIN, C_LSBRCK_0_RSBRCK_;
}

\problem {
(-1*d + 3 >= 0 & cout1 >= 0 & a_LSBRCK_1_RSBRCK_ >= 0 & ! (CIN = 0 & BITADDER_LSBRCK_0_RSBRCK__S1 = 0 & BITADDER_LSBRCK_0_RSBRCK__C2 != 0) & ! (CIN = 0 & cin + -1 != 0) & ! (BITADDER_LSBRCK_1_RSBRCK__C2 = 0 & BITADDER_LSBRCK_1_RSBRCK__S1 != 0) & ! (CIN != 0 & cin != 0) & ! (B_LSBRCK_1_RSBRCK_ != 0 & b_LSBRCK_1_RSBRCK_ != 0))
->
(-1*d + 3 >= 0 & cout1 >= 0 & a_LSBRCK_1_RSBRCK_ >= 0 & ! (CIN = 0 & BITADDER_LSBRCK_0_RSBRCK__S1 = 0 & BITADDER_LSBRCK_0_RSBRCK__C2 != 0) & ! (CIN = 0 & cin + -1 != 0) & ! (BITADDER_LSBRCK_1_RSBRCK__C2 = 0 & BITADDER_LSBRCK_1_RSBRCK__S1 != 0) & ! (CIN != 0 & cin != 0) & ! (B_LSBRCK_1_RSBRCK_ != 0 & b_LSBRCK_1_RSBRCK_ != 0))
}
